Nuprl Definition : inr def 13,42
inr x  is Primitive 
latex

Upcore 1, core 1

origin